Search Results

Documents authored by Weil, Pascal

Document
DOI: 10.4230/LIPIcs.CONCUR.2022.28
Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages

Authors: Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
One of the main motivations for this work is to obtain a distributed Krohn-Rhodes theorem for Mazurkiewicz traces. Concretely, we focus on the recently introduced operation of local cascade product of asynchronous automata and ask if every regular trace language can be accepted by a local cascade product of "simple" asynchronous automata. Our approach crucially relies on the development of a local and past-oriented propositional dynamic logic (LocPastPDL) over traces which is shown to be expressively complete with respect to all regular trace languages. An event-formula of LocPastPDL allows to reason about the causal past of an event and a path-formula of LocPastPDL, localized at a process, allows to march along the sequence of past-events in which that process participates, checking for local regular patterns interspersed with local tests of other event-formulas. We also use additional constant formulas to compare the leading process events from the causal past. The new logic LocPastPDL is of independent interest, and the proof of its expressive completeness is rather subtle. Finally, we provide a translation of LocPastPDL formulas into local cascade products. More precisely, we show that every LocPastPDL formula can be computed by a restricted local cascade product of the gossip automaton and localized 2-state asynchronous reset automata and localized asynchronous permutation automata.
Cite as

Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{adsul_et_al:LIPIcs.CONCUR.2022.28,
  author =	{Adsul, Bharat and Gastin, Paul and Sarkar, Saptarshi and Weil, Pascal},
  title =	{{Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.28},
  URN =		{urn:nbn:de:0030-drops-170915},
  doi =		{10.4230/LIPIcs.CONCUR.2022.28},
  annote =	{Keywords: Mazurkiewicz traces, propositional dynamic logic, regular trace languages, asynchronous automata, cascade product, Krohn Rhodes theorem}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.19
Wreath/Cascade Products and Related Decomposition Results for the Concurrent Setting of Mazurkiewicz Traces

Authors: Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We develop a new algebraic framework to reason about languages of Mazurkiewicz traces. This framework supports true concurrency and provides a non-trivial generalization of the wreath product operation to the trace setting. A novel local wreath product principle has been established. The new framework is crucially used to propose a decomposition result for recognizable trace languages, which is an analogue of the Krohn-Rhodes theorem. We prove this decomposition result in the special case of acyclic architectures and apply it to extend Kamp’s theorem to this setting. We also introduce and analyze distributed automata-theoretic operations called local and global cascade products. Finally, we show that aperiodic trace languages can be characterized using global cascade products of localized and distributed two-state reset automata.
Cite as

Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Wreath/Cascade Products and Related Decomposition Results for the Concurrent Setting of Mazurkiewicz Traces. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{adsul_et_al:LIPIcs.CONCUR.2020.19,
  author =	{Adsul, Bharat and Gastin, Paul and Sarkar, Saptarshi and Weil, Pascal},
  title =	{{Wreath/Cascade Products and Related Decomposition Results for the Concurrent Setting of Mazurkiewicz Traces}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.19},
  URN =		{urn:nbn:de:0030-drops-128319},
  doi =		{10.4230/LIPIcs.CONCUR.2020.19},
  annote =	{Keywords: Mazurkiewicz traces, asynchronous automata, wreath product, cascade product, Krohn Rhodes decomposition theorem, local temporal logic over traces}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.29
The Quantifier Alternation Hierarchy of Synchronous Relations

Authors: Diego Figueira, Varun Ramanathan, and Pascal Weil

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
The class of synchronous relations, also known as automatic or regular, is one of the most studied subclasses of rational relations. It enjoys many desirable closure properties and is known to be logically characterized: the synchronous relations are exactly those that are defined by a first-order formula on the structure of all finite words, with the prefix, equal-length and last-letter predicates. Here, we study the quantifier alternation hierarchy of this logic. We show that it collapses at level Sigma_3 and that all levels below admit decidable characterizations. Our results reveal the connections between this hierarchy and the well-known hierarchy of first-order defined languages of finite words.
Cite as

Diego Figueira, Varun Ramanathan, and Pascal Weil. The Quantifier Alternation Hierarchy of Synchronous Relations. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 29:1-29:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{figueira_et_al:LIPIcs.MFCS.2019.29,
  author =	{Figueira, Diego and Ramanathan, Varun and Weil, Pascal},
  title =	{{The Quantifier Alternation Hierarchy of Synchronous Relations}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{29:1--29:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.29},
  URN =		{urn:nbn:de:0030-drops-109735},
  doi =		{10.4230/LIPIcs.MFCS.2019.29},
  annote =	{Keywords: synchronous relations, automatic relations, first-order logic, characterization, quantifier alternation}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.STACS.2008
LIPIcs, Volume 1, STACS'08, Complete Volume

Authors: Susanne Albers and Pascal Weil

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract
LIPIcs, Volume 1, STACS'08, Complete Volume
Cite as

25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{albers_et_al:LIPIcs.STACS.2008,
  title =	{{LIPIcs, Volume 1, STACS'08, Complete Volume}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008},
  URN =		{urn:nbn:de:0030-drops-40958},
  doi =		{10.4230/LIPIcs.STACS.2008},
  annote =	{Keywords: LIPIcs, Volume 1, STACS'08, Complete Volume}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.426
The FO2 alternation hierarchy is decidable

Authors: Manfred Kufleitner and Pascal Weil

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
We consider the two-variable fragment FO2[<] of first-order logic over finite words. Numerous characterizations of this class are known. Therien and Wilke have shown that it is decidable whether a given regular language is definable in FO2[<]. From a practical point of view, as shown by Weis, FO2[<] is interesting since its satisfiability problem is in NP. Restricting the number of quantifier alternations yields an infinite hierarchy inside the class of FO2[<]-definable languages. We show that each level of this hierarchy is decidable. For this purpose, we relate each level of the hierarchy with a decidable variety of finite monoids. Our result implies that there are many different ways of climbing up the FO2[<]-quantifier alternation hierarchy: deterministic and co-deterministic products, Mal'cev products with definite and reverse definite semigroups, iterated block products with J-trivial monoids, and some inductively defined omega-term identities. A combinatorial tool in the process of ascension is that of condensed rankers, a refinement of the rankers of Weis and Immerman and the turtle programs of Schwentick, Therien, and Vollmer.
Cite as

Manfred Kufleitner and Pascal Weil. The FO2 alternation hierarchy is decidable. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 426-439, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kufleitner_et_al:LIPIcs.CSL.2012.426,
  author =	{Kufleitner, Manfred and Weil, Pascal},
  title =	{{The FO2 alternation hierarchy is decidable}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{426--439},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.426},
  URN =		{urn:nbn:de:0030-drops-36888},
  doi =		{10.4230/LIPIcs.CSL.2012.426},
  annote =	{Keywords: first-order logic, regular language, automata theory, semigroup, ranker}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.STACS.2008.1378
Abstracts Collection -- 25th International Symposium on Theoretical Aspects of Computer Science

Authors: Susanne Albers and Pascal Weil

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract
The Symposium on Theoretical Aspects of Computer Science (STACS) is held alternately in France and in Germany. The conference of February 21-23, 2008, held in Bordeaux, is the 25th in this series. Previous meetings took place in Paris (1984), Saarbr\"{u}cken (1985), Orsay (1986), Passau (1987), Bordeaux (1988), Paderborn (1989), Rouen (1990), Hamburg (1991), Cachan (1992), W\"{u}rzburg 1993), Caen (1994), M\"{u}nchen (1995), Grenoble (1996), L\"{u}beck (1997), Paris (1998), Trier (1999), Lille (2000), Dresden (2001), Antibes (2002), Berlin (2003), Montpellier (2004), Stuttgart (2005), Marseille (2006) and Aachen (2007).
Cite as

25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. i-xxviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{albers_et_al:LIPIcs.STACS.2008.1378,
  author =	{Albers, Susanne and Weil, Pascal},
  title =	{{Abstracts Collection -- 25th International Symposium on Theoretical Aspects of Computer Science}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{i--xxviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1378},
  URN =		{urn:nbn:de:0030-drops-13780},
  doi =		{10.4230/LIPIcs.STACS.2008.1378},
  annote =	{Keywords: Symposium, theoretical computer science, algorithms and data structures, automata and formal languages, computational and structural complexity, logic in computer science, applications}
}
Document
DOI: 10.4230/LIPIcs.STACS.2008.1326
Preface -- 25th International Symposium on Theoretical Aspects of Computer Science

Authors: Susanne Albers and Pascal Weil

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract
The interest in STACS has remained at a high level over the past years. The STACS 2008 call for papers led to approximately 200 submissions from 38 countries. Each was assigned to at least three program committee members. The program committee held a 2-week long electronic meeting at the end of November, to select 54 papers. As co-chairs of this committee, we would like to sincerely thank its members and the many external referees for the valuable work they put into the reviewing process. The overall very high quality of the papers that were submitted to the conference made this selection a difficult task. We would like to express our thanks to the three invited speakers, Maxime Crochemore, Thomas Schwentick and Mihalis Yannakakis, for their contributions to the proceedings. Special thanks are due to A. Voronkov for his EasyChair software (www.easychair.org) which gives the organisers of conferences such as STACS a remarkable level of comfort; to Ralf Klasing for helping us explore the many possibilities of this brilliant software; to Emilka Bojanczyk for the design of the STACS poster, proceedings and logo; and to the members of the Organizing Committee, chaired by David Janin. An innovation in this year's STACS is the electronic format of the publication. A printed version was also available at the conference, with ISBN 978-3-939897-06-4. The electronic proceedings are available through several portals, and in particular through HAL and DROPS. HAL is an electronic repository managed by several French research agencies, and DROPS is the Dagstuhl Research Online Publication Server. We want to thank both these servers for hosting the proceedings of STACS and guaranteeing them perennial availability. The rights on the articles in the proceedings are kept with the authors and the papers are available freely, under a Creative Commons license (see www.stacs-conf.org/faq.html for more details).
Cite as

Susanne Albers and Pascal Weil. Preface -- 25th International Symposium on Theoretical Aspects of Computer Science. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{albers_et_al:LIPIcs.STACS.2008.1326,
  author =	{Albers, Susanne and Weil, Pascal},
  title =	{{Preface -- 25th International Symposium on Theoretical Aspects of Computer Science}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{1--10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1326},
  URN =		{urn:nbn:de:0030-drops-13263},
  doi =		{10.4230/LIPIcs.STACS.2008.1326},
  annote =	{Keywords: Symposium, theoretical computer science, algorithms and data structures, automata and formal languages, computational and structural complexity, logic in computer science, applications}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact